Nuprl Lemma : rng_times_over_plus
13,42
postcript
pdf
r
:Rng,
a
,
b
,
c
:|
r
|.
(
a
* (
b
+
r
c
)) = ((
a
*
b
) +
r
(
a
*
c
))
|
r
| & ((
b
+
r
c
) *
a
) = ((
b
*
a
) +
r
(
c
*
a
))
|
r
|
latex
Up
rings
1
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
BiLinear(
T
;
pl
;
tm
)
Lemmas
rng
wf
,
rng
all
properties
origin
r:Rng, a, b, c:|r|.
|r| & ((b +r c) * a) = ((b * a) +r (c * a)) |r| r:Rng, a, b, c:|r|.
|r| & ((b +r c) * a) = ((b * a) +r (c * a)) |r| Tx:A. B(x)